package pa14.proj.boundschecker.main;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;

import soot.Body;
import soot.G;
import soot.Local;
import soot.Unit;
import soot.Value;
import soot.ValueBox;
import soot.jimple.AssignStmt;
import soot.jimple.NewArrayExpr;
import soot.jimple.internal.ImmediateBox;
import soot.jimple.internal.InvokeExprBox;
import soot.jimple.internal.JimpleLocal;
import soot.jimple.internal.JimpleLocalBox;
import soot.jimple.internal.RValueBox;
import soot.toolkits.graph.ExceptionalUnitGraph;
import soot.toolkits.scalar.ForwardFlowAnalysis;
import soot.util.Chain;

public class BoundsCheckerAnalysis
			extends ForwardFlowAnalysis<Unit, HashMap<Value, List<Integer>>> {
	
	private boolean dl, om;
		
	private HashMap<Value, Integer> ranges = null;
	private HashMap<Value, Value> synonyms = null;
	private List<String> violations = null;
	private HashSet<Value> localArrayVars = null;

	public BoundsCheckerAnalysis(ExceptionalUnitGraph graph) {
		super(graph);
		this.dl = false;
		this.om = true;
		this.violations = new ArrayList<String>();
		this.ranges = new HashMap<Value, Integer>();
		this.synonyms = new HashMap<Value, Value>();
		this.localArrayVars = getLocalArrayVars(graph.getBody());
			
		
		//start analysis
		doAnalysis();
	}

	@Override
	protected void flowThrough(	HashMap<Value, List<Integer>> in,
								Unit thisStmt,
								HashMap<Value, List<Integer>> out) {
		
		if(dl)print("Statement:" + thisStmt, 1);
		if(dl)print("Useboxes:", 2);
		List<ValueBox> useBoxes = thisStmt.getUseBoxes();
		if(dl)for(ValueBox vb: useBoxes){
			print(vb, 3);
		}
		//-------------------

		out.clear();
		out.putAll(in);
		
		if(isCreationStatement(thisStmt)){
			if(dl)print(" is a creation statement", 2);
			List<ValueBox> defVars = thisStmt.getDefBoxes();
			ValueBox definedVar = defVars.get(0);
			Integer definedIndexRange = getDefinedIndexRange(thisStmt);
			if(dl)print(" got the defined range as: " + definedIndexRange, 2);
			//out.clear();
			//out.putAll(in);
			if(ranges.containsKey(definedVar.getValue())){
				Integer inRange = ranges.get(definedVar.getValue());
				Integer obtainedRange = definedIndexRange;
				if(obtainedRange < inRange){
					ranges.put(definedVar.getValue(), obtainedRange);
				}
			}else{
				ranges.put(definedVar.getValue(), definedIndexRange);
			}
			if(dl)printMap2(ranges, "ranges", 5);
		}
		
		
		if(hasConstantAssignment(thisStmt)){
			//If a constant is assigned to the variable, generate the variable with that value
			if(dl)print("has a constant assignment. let's check", 4);
			if(dl)printMap(in, "in", 5);
			Value definedValue = getDefinedVariable(thisStmt);
			Integer definedRange = getIntegerValueFromVB(thisStmt);
			//generate this value
			if(out.containsKey(definedValue)){
				List<Integer> l1 = out.get(definedValue);
				l1.add(definedRange);
				out.put(definedValue, l1);
			}else{
				List<Integer> list = new ArrayList<Integer>();
				list.add(definedRange);
				out.put(definedValue, list);
			}

			printMap(out, "out", 5);
		}
		
		if(isArrayAssignment(thisStmt)){
			if(dl)print("has array assignment!", 4);
			Value lValue = null, rValue = null;
			
			List<ValueBox> lValues = thisStmt.getDefBoxes();
			if(lValues.size() != 0){
				lValue = lValues.get(0).getValue();
			}
			List<ValueBox> rValues = thisStmt.getUseBoxes();
			if(rValues.size() != 0){
				rValue = rValues.get(0).getValue();
			}
			
			if(synonyms.get(rValue)!= null){
				synonyms.put(lValue, synonyms.get(rValue));
			}else if(lValue != null && rValue != null){
				synonyms.put(lValue, rValue);
			}
		}else if(hasSingleValuePassingAssignment(thisStmt)){
			if(dl)print("has single value passing assignment", 5);
			//when variables are assigned to other variables
			// basically the new variable is generated and put back into the hash map

			Value usedVariable = thisStmt.getUseBoxes().get(0).getValue();
			Value definedVariable = getDefinedVariable(thisStmt);
			List<Integer> pairValue = out.get(usedVariable);
			out.put(definedVariable, pairValue);
			printMap(out, "out", 5);
		}else if(hasValueChangingPassingAssignment(thisStmt)){
			if(dl)print("Has a value changing passing assignment", 5);
			//int valueChangers = getValueChangingPassingAssignment(thisStmt);
			
			Value usedVariable = getModifiedOfValueChangingAssignment(thisStmt);
			Value definedVariable = getDefinedVariable(thisStmt);
			int modification = getModifyOfValueChangingAssignment(thisStmt);
			List<Integer> finalValues = new ArrayList<Integer>();
			List<Integer> originalValues = in.get(usedVariable);
			for(Integer val: originalValues){
				finalValues.add(val + modification);
			}
			out.put(definedVariable, finalValues);
			printMap(out, "out", 5);
		}
		
		if(hasAccessStatement(thisStmt)){
			if(dl)print("hasAnAccessStatement", 3);
			Value[] accessVars = getAccessStatements(thisStmt);
			if(accessVars == null)if(dl)print("no accessvars received", 3);
			Value arrayVar = accessVars[0];
			Value indexVar = accessVars[1];
			
			//Value definedValue = getDefinedVariable(thisStmt);
			//Pair<Value, Integer> specifiedVar = in.get(definedValue);
			
			Integer specifiedRange = null;
			if(ranges.containsKey(arrayVar)){
				specifiedRange = ranges.get(arrayVar);
			}else{
				specifiedRange = ranges.get(synonyms.get(arrayVar));
			}
			List<Integer> definedRanges = in.get(indexVar);
			for(Integer range: definedRanges){
				if((range.intValue() >= 0) && (range.intValue() < specifiedRange.intValue())){
					if(dl)print("--RANGE IS OKAY--", 3);
				}else{
					if(dl)print("--RANGE IS FAULTY--", 3);
					Value actualArrayVar = synonyms.get(arrayVar);
					violations.add("index value " + range + " is out of bounds for the array var '" + actualArrayVar + "'\n\t\t\tat statement: "+ thisStmt);
				}
			}
		}
		
		
		
		//--------------------
	}
	
	private boolean hasValueChangingPassingAssignment(Unit thisStmt) {
		if ((thisStmt instanceof AssignStmt) && !hasAccessStatement(thisStmt)){
			List<ValueBox> useBoxes = thisStmt.getUseBoxes();
			boolean	hasLocalVar = false, hasModifier = false;
			for(ValueBox vb: useBoxes){
				if(vb instanceof ImmediateBox){
					if(vb.getValue() instanceof JimpleLocal){
						if(dl)print(vb  + ": that's the local we have!", 6);
						hasLocalVar = true;
					}
					if((vb instanceof ImmediateBox) && !(vb.getValue() instanceof JimpleLocal)){
						if(dl)print(vb + ": this value is being detected as integer!", 6);
						hasModifier = true;
					}
				}
			}
			if(hasLocalVar && hasModifier){
				return true;
			}
		}
		
		return false;
	}

	private int getModifyOfValueChangingAssignment(Unit thisStmt) {
		List<ValueBox> useBoxes = thisStmt.getUseBoxes();

		for(ValueBox vb: useBoxes){
			if(vb instanceof ImmediateBox){
				if(!(vb.getValue() instanceof JimpleLocal)){
					if(dl)print(vb + ": this value is being detected as integer!", 6);
					return Integer.parseInt(vb.getValue().toString());
				}
			}
		}
		return 0;
	}
	
	private Value getModifiedOfValueChangingAssignment(Unit thisStmt) {
		List<ValueBox> useBoxes = thisStmt.getUseBoxes();
		for(ValueBox vb: useBoxes){
			if(vb instanceof ImmediateBox){
				if(vb.getValue() instanceof JimpleLocal){
					if(dl)print(vb  + ": that's the local we have!", 6);
					return vb.getValue();
				}
			}
		}
		return null;
	}

	private boolean isArrayAssignment(Unit thisStmt) {
		List<ValueBox> rValue = thisStmt.getUseBoxes();
		if(rValue.size() == 1){
			if(localArrayVars.contains(rValue.get(0).getValue())){
				return true;
			}
		}
		return false;
	}
	
	protected boolean isCreationStatement(Unit thisStmt){
		List<ValueBox> useBoxes = thisStmt.getUseBoxes();
		
		for(ValueBox useBox: useBoxes){
			if(useBox instanceof RValueBox){
				Value boxValue = useBox.getValue();
				if(boxValue instanceof NewArrayExpr){
					return true;
				}
			}
		}
		
		return false;
	}
	
	private Integer getDefinedIndexRange(Unit thisStmt) {
		ValueBox newArrayElement = thisStmt.getUseBoxes().get(0);
		Value value = newArrayElement.getValue();
		Integer newIndex = Integer.parseInt(value.toString());
		return newIndex;
	}
	
	private boolean isVBInteger(ValueBox vb) {
		if(!(vb.getValue() instanceof JimpleLocal) && vb.getValue().getType().toString().equals("int")){
			return true;
		}
		return false;
	}
	
	private int getIntegerValueFromVB(Unit thisStmt) {
		return Integer.parseInt(thisStmt.getUseBoxes().get(0).getValue().toString());
	}

	protected boolean hasAccessStatement(Unit thisStmt){
		List<ValueBox> accessStmts = thisStmt.getUseBoxes();
		boolean hasArrayVar = false, hasIndexVar = false, hasInvoke = false;

		for(ValueBox v: accessStmts){
			if(v instanceof JimpleLocalBox){
				hasArrayVar = true;
			}
			if(v instanceof ImmediateBox){
				hasIndexVar = true;
			}
			if(v instanceof InvokeExprBox){
				hasInvoke = true;
			}
		}
		return (hasArrayVar && hasIndexVar && !hasInvoke);
	}

	private Value[] getAccessStatements(Unit thisStmt) {
		List<ValueBox> accessStmts = thisStmt.getUseBoxes();
		
		Value arrayVar = null, indexVar = null;
		for(ValueBox v: accessStmts){
			if(v instanceof JimpleLocalBox){
				arrayVar = v.getValue();
			}
			if(v instanceof ImmediateBox){
				indexVar = v.getValue();
			}
		}
		Value[] retValue = new Value[]{arrayVar, indexVar};
		return retValue;
	}

	private boolean hasSingleStaticVariableAssignment(Unit thisStmt) {
		return ((thisStmt instanceof AssignStmt) && (thisStmt.getUseBoxes().size() == 1));
	}
	private boolean hasSingleValuePassingAssignment(Unit thisStmt){
		return ((thisStmt instanceof AssignStmt)
				&& !hasConstantAssignment(thisStmt)
				&& (thisStmt.getUseBoxes().size() == 1)
				&& (thisStmt.getUseBoxes().get(0) instanceof RValueBox));
	}

	private Value getDefinedVariable(Unit thisStmt) {
		return thisStmt.getDefBoxes().get(0).getValue();
	}

	private boolean hasConstantAssignment(Unit thisStmt) {
		return hasSingleStaticVariableAssignment(thisStmt) && isVBInteger(thisStmt.getUseBoxes().get(0));
	}

	@Override
	protected void copy(HashMap<Value, List<Integer>> source,
						HashMap<Value, List<Integer>> dest) {
		dest.clear();
		dest.putAll(source);
	}

	@Override
	protected HashMap<Value, List<Integer>> entryInitialFlow() {
		return new HashMap<Value, List<Integer>>();
	}

	@Override
	protected void merge(	HashMap<Value, List<Integer>> in1,
							HashMap<Value, List<Integer>> in2,
							HashMap<Value, List<Integer>> out) {
		out.clear();
		
		//merge values obtained from both sets
		out.putAll(in1);
		for(Value v: in2.keySet()){
			if(in1.containsKey(v)){
				List<Integer> finalList = new ArrayList<Integer>();
				if(dl)printMap(in1, "in1", 5);
				if(dl)printMap(in2, "in2", 5);
				finalList.addAll(in1.get(v));
				finalList.addAll(in2.get(v));
				out.put(v, finalList);
			}else{
				out.put(v, in2.get(v));
			}
		}
	}

	@Override
	protected HashMap<Value, List<Integer>> newInitialFlow() {
		return new HashMap<Value, List<Integer>>();
	}

	public void printResults() {
		if(om)print("===Printing results===", 0);
		if(violations.size() != 0){
			for(String s: violations){
				if(om)print(s, 1);
			}
		}else{
			if(om)print("_No violations detected!_", 1);
		}
	}
	
	protected void print(Object str, int n){
		while(n-- != 0){
			G.v().out.print("\t");
		}
		G.v().out.println(str);
	}
	
	protected void printMap(HashMap<Value, List<Integer>> unit, String name, int n){
		if(dl)print("Printing values for: " + name, n);
		if(dl)for(Value v: unit.keySet()){
			print("|> " + v + "\t--> [" + unit.get(v) + "]", n);
		}
	}
	
	protected void printMap2(HashMap<Value, Integer> unit, String name, int n){
		if(dl)print("Printing values for: " + name, n);
		if(dl)for(Value v: unit.keySet()){
			print("|> " + v + "\t--> [" + unit.get(v) + "]", n);
		}
	}
	
	protected HashSet<Value> getLocalArrayVars(Body body) {
		boolean verbose = dl;
		
		//SootMethod thisMethod = body.getMethod();
		Chain<Local> localVars = body.getLocals();
		HashSet<Value> arrayVars = new HashSet<Value>();
		for(Local l: localVars){
			Value g = (Value)l;
			if(verbose){	print("got a localvar: " + l + " --type: " + l.getType(), 1);}
			String localVarType = l.getType().toString();
			//print(localVarType.substring(localVarType.length() - 2), 3);
			if(localVarType.substring(localVarType.length() - 2).equals("[]")){
				if(verbose){	print(" this is definitely an array", 3);}
				arrayVars.add(g);
			}
		}
		if(dl)print("Printing values for: LocalArrayVars", 5);
		if(dl)for(Value v: arrayVars){
			print("|> " + v , 5);
		}
		return arrayVars;
	}

}
